K. Sasaki; "Löb's Axiom and Cut-Elimination Theorem"

Memo

いくつかまとめ直している．

Notation

以下

論理$ \LambdaのHilbert流演繹体系を$ \mathfrak{H}_\Lambda

論理$ \Lambdaのカット無しシークエント計算体系を$ \mathfrak{S}_\Lambda

カットなしのシークエント計算体系$ \mathfrak{S}にカット規則を追加したシーケント体系を$ \mathfrak{S}^\mathrm{C}と表記する．

Hilbert流演繹体系$ \mathfrak{H}，シークエント計算体系$ \mathfrak{S}で$ Aが証明可能であることを$ \vdash_\mathfrak{H} A，$ \vdash_\mathfrak{S} Aと表す．

様相論理の体系には一様代入則があるとする．

正規様相論理K4のHilbert流演繹体系$ \mathfrak{H}_\mathsf{K4} = \mathfrak{H}_\mathsf{K} + \lbrack \Box p \to \Box\Box p \rbrack

すなわち$ \mathfrak{H}_\mathsf{K4}は正規様相論理Kに様相論理の公理4を追加した体系とする．

様相論理GLのHilbert流演繹体系$ \mathfrak{H}_\mathsf{GL} = \mathfrak{H}_\mathsf{K4} + \lbrack \Box (\Box p \to p) \to \Box p \rbrack

一般のものと違い$ \sf K4の上に追加していることに注意．

$ \mathfrak{S}_\mathsf{K4} = \mathfrak{S}_\mathsf{PL} + \dfrac{\Gamma, \Box\Gamma \rArr A}{\Box\Gamma \rArr \Box A}

追加された規則は$ \Box_\mathsf{K4}規則という．

$ \mathfrak{S}_\mathsf{GL} = \mathfrak{S}_\mathsf{PL} + \dfrac{\Box A, \Gamma, \Box\Gamma \rArr A}{\Box\Gamma \rArr \Box A}

追加された規則は$ \Box_\mathsf{GL}規則という．

Lem: $ \sf K4のシーケント計算について

$ \vdash_{\mathfrak{S}_\mathsf{K4}} \rArr A \iff \vdash_{\mathfrak{H}_\mathsf{K4}} A

カット無し$ \sf K4シーケント計算体系とHilbert流は証明能力が等価

ref:?

$ \vdash_{\mathfrak{S}^\mathrm{C}_\mathsf{K4}} \Gamma \rArr \Delta \implies \vdash_{\mathfrak{S}_\mathsf{K4}} \Gamma \rArr \Delta

$ \sf K4のシーケント計算体系ではカット除去定理が成り立つ．

Lem: $ \sf GLのシーケント計算について

$ \vdash_{\mathfrak{S}^\mathrm{C}_\mathsf{GL}} \rArr A \iff \vdash_{\mathfrak{H}_\mathsf{GL}} A

カット有り$ \sf GLシーケント計算体系とHilbert流は証明能力が等価．

今後示す目標は以下のThm1/カット除去定理である．

$ \vdash_{\mathfrak{S}^\mathrm{C}_\mathsf{GL}} \Gamma \rArr \Delta \implies \vdash_{\mathfrak{S}_\mathsf{GL}} \Gamma \rArr \Delta